FIELD OF THE INVENTION
The present invention relates to a method and an apparatus for verifying whether or not a model of a logical device provided with functional specification by a finite state machine.
A finite state machine is popularly used as a mathematical model of a synchronous order machine and protocol, and also relates to a method of verifying a synchronous sequential circuit and protocol. A well-known method of verifying whether or not the functional design of a logical device correctly represents its specification is a model checking method (refer to reference documents 2 and 5). This method mathematically proves that a finite state machine satisfies or does not satisfy the specification represented by a temporal logic.
The verifying operation of a logical device in the model checking method includes various steps from verifying abstract specification to operating a practical circuit. In these steps, since errors can be more easily detected in the verification of functional specification at the earliest stage in the logical device, it has been expected to perform a verifying process at a high speed and with high precision. Furthermore, the verifying process has been expected to be performed on a complicated logical device whose memory capacity reaches its limit in a common method.
Described below is the conventional technology.
.sctn.1: Explanation of conventional technology (1).
The above described finite state machine is defined as a finite automation with output. A common format of the finite state machine is obtained by the following equation (1). EQU M=(Q, .SIGMA., .PHI., .delta., .lambda., I) (1)
Each of the symbols has the following meaning.
Q: state set (finite) PA1 .SIGMA.: input alphabet (finite) PA1 .PHI.: output alphabet (finite) PA1 .delta.: transition relation function PA1 .lambda.: output relation function PA1 I: initial state set
The above described transition relation function .lambda. is a function which determines the next state. It is set to 1 when the current state can be transient to the next state if the current state and an input are entered when the current state, the next state and an input can be entered to represent a nondeterministic transition. Otherwise, it is set to 0. When the transition is deterministic, the state transition can be represented as a function for obtaining the next state by the current state and an input. The above described output relation function .lambda. similarly corresponds to the case where an output is nondeterministic.
Basically, all synchronous sequential circuits can be modelled by the finite state machine. Therefore, when a logical device is designed, the finite state machine is popularly used as specification. For example, in synthesizing a logic, a state is commonly represented by a flip-flop circuit or a register by a synthesizing system converting the description of the specification of a device written in a design description language into a finite state machine, or a transition relation function .delta. and an output relation function .lambda. is commonly represented by a combinational circuit.
The basic logic of the above described finite state machine is described in detail in chapter 2 of the reference document 6. Verifying a device specified as a finite state machine is to check whether or not the device correctly represents the state transition of the finite state machine. An applicable technology to attain the verification can be logical simulation and formal verification.
The above described logical simulation is a process of simulating an operation by applying an appropriate input to a model of a device (description in design description language, gate level circuit chart, etc.). It is confirmed that an output obtained in the process matches the value obtained by the original finite state machine.
The above described formal verification is an approach to mathematically prove whether or not the property satisfied by the original finite state machine is completely satisfied by the model of the device. Typical examples are a symbol model check, symbol simulation, etc. The formal verification is described in detail in the reference documents 5, 3, 11, 13, and 8.
The above described formal verification (formal verification method) refers to a technology under development from the research stage to the practical stage, and several cases where the method is used in processor design verification have been reported. Among them, the symbol model checking method (refer to reference document 2) for verifying a control logic is considered to be the most practical method.
.sctn.2: Explanation of conventional technology (2) . . . refer to FIG. 1A.
FIG. 1A shows the conventional technology, that is, an example (1) of the finite state machine. In the above described formal verification methods, the symbol model checking method represents a logical device model of the Kripke structure using a logical function, checks whether or not a non-blank state set which satisfy the specification represented by a computation tree logic exist.
The Kripke structure is a kind of nondeterministic finite automaton represented by the following equation (2) using the finite set S of a state, the transition relation R of a state, the set S.sub.0 of an initial state point, and the set L of an atomic proposition which is true in each state. EQU K=(S, R, S.sub.0, L) (2)
The computation tree logic is a kind of a temporal logic, and is represented by an operator A indicating `universal`, an operator E indicating `existential`, a temporal operator F indicating `future`, a temporal operator G indicating `global`, a temporal operator X indicating `next`, and a temporal operator U indicating `until` in addition to a common logic operator.
For example, the temporal operator AGa indicates that the logical expression a exists in all state sets reachable from the initial state. In this case, in a model of a logical device, all paths reachable from the initial state are traced, and it is checked whether or not all the paths can reach the state in which the logical expression a exists.
That is, the verifying operation in the symbol model checking method is an operation of tracing the state transition of the Kripke structure and confirming whether or not the computation tree logic indicating the specification exists in each state. This operation refers to a set operation for obtaining the smallest floating point or the largest floating point in a model according to a computation tree logic expression.
The above described set operation can be realized by combining an image computation Image ({q}) for obtaining a state set reachable from a state set {q} in one state transition process with an inverse image computation Image.sup.-1 ({q}) for obtaining a state set reachable to a state set {q} in one state transition process.
For example, in the example of the finite state machine represented by a state transition between nine states q.sub.0 through q.sub.8 as shown in FIG. 1A, examples of results of the image computation and the inverse image computation are represented by the following equations (3) through (6). EQU Image ({q.sub.0 })={q.sub.0, q.sub.1, q.sub.2, q.sub.3 } (3) EQU Image ({q.sub.3, q.sub.8 })={q.sub.2, q.sub.3, q.sub.5, q.sub.6, q.sub.8 }(4) EQU Image.sup.-1 ({q.sub.0 })={q.sub.0, q.sub.1 } (5) EQU Image.sup.-1 ({q.sub.5 })={q.sub.1, q.sub.2, q.sub.3, q.sub.4 }(6)
In the finite state machine shown in FIG. 1A, when the temporal logic AFp using the logical expression p indicating the state q.sub.7 is verified, the image computation is sequentially repeated from the initial state q.sub.0, and it is checked whether or not all paths transient from the initial state can actually reach the state q.sub.7. When the temporal logic EFp is verified, the inverse image computation is repeated from the state q.sub.7, and it is checked whether or not there is a path reaching the initial state q.sub.0.
In a common actual symbol model checking method, a set operation is replaced with a logical function process (refer to reference document 5), and the logical function process becomes more efficient by representing the logical function by a binary decision diagram (refer to reference document 1).
.sctn.3: Explanation of conventional technology (3) . . . Refer to FIGS. 1B through 1H.
FIG. 1B shows the explanation (2) of the conventional technology. FIG. 1C shows the explanation (3) of the conventional technology. FIG. 1D shows the explanation (4) of the conventional technology. FIG. 1E shows the explanation (5) of the conventional technology. FIG. 1F shows the explanation (6) of the conventional technology. FIG. 1G shows the explanation (7) of the conventional technology. FIG. 1H shows the explanation (8) of the conventional technology. In the above described symbol model checking method, a property verification device (refer to Tokuganhei 8-220005) capable of both reducing the scale of memory and shortening a process time has already been suggested. This conventional technology is described below by referring to FIGS. 1B through 1H.
In FIG. 1B, the property verification device converts the computation tree logic expression accepted through an input receipt unit 211 as a logical expression input means into a single path representation through a single path representation conversion unit 212. Furthermore, the representation is converted by a procedure string conversion unit 213 into a procedure string described later and then provided for process by a set operation unit 214. A determining unit 215 determines whether or not the obtained state set is empty. Thus, the input property can be verified.
In the input receipt unit 211, an operator determination unit 221 transmits the computation tree logic expression to an initial state addition unit 223 directly or through a negating unit 222 depending on the leading operator in the received computation tree logic expression. When the leading operator is the operator A indicating `universal`, the operator determination unit 221 transmits the entire computation tree logic expression to the negating unit 222. When the leading operator is the operator E indicating `existential`, it transmits the expression to the negating unit 222.
The negating unit 222 negates the entire computation tree logic expression received from the operator determination unit 221, furthermore prepares the computation tree logic expression by transforming a necessary equation according to a logical operation rule, and transmits the obtained computation tree logic expression to the initial state addition unit 223. The initial state addition unit 223 transmits the computation tree logic expression to the single path representation conversion unit 212 as a starting state of the verifying operation by adding a proposition logical expression corresponding to the initial state to the head of the received computation tree logic expression.
In the single path representation conversion unit 212, an expression transforming unit 224 receives a computation tree logic expression from the above described input receipt unit 211, transforms the computation tree logic expression according to the transform rule stored in a transform rule storage unit 225, and converts is into a single path representation. The transform rule storage unit 225 stores the conversion rule R represented by the following equations (7) through (10) using, as the procedure for converting a computation tree logic expression into a single path representation, the proposition logical expressions p and q indicating a state set, and a partial expression f of the above described computation tree logic expression. EQU R(pEX f)=pR(f) (7) EQU R(pEF f)={R(pf), pTrue*R(f)} (8) EQU R(pEG q)=(pf)q .omega. (9) EQU R(pE(q.orgate.f)={R(pf), pq*R(f)} (10)
In the above listed equations (7) through (10), the finite and infinite repetition of the proposition logical expression p is represented by an index symbols * and .omega.. Each case group is enclosed by {}. The expression transforming unit 224 detects the portion applicable to the above described conversion rule in the received computation tree logic expression. An applicable conversion rule is applied to perform a conversion process to perform a converting process for a unit path representation.
The single path representation refers to a single non-branch state set string or a state set string obtained by linking a state set string which is an infinite loop to a single non-branch state set string. The state set S of a single path representation s is defined as follows using the set P of the proposition logical expression indicating an optional state set.
1: The state set where p.epsilon.P is a single path representation.
2: The connection ps between the state set where p.epsilon.P and the state set string s where s.epsilon.S is a single path representation.
3: The infinite repetition p.omega. of the state set p where p.epsilon.P is a single path representation.
4: The connection p* between the finite repetition p* of the state set p where p.epsilon.P and the state set string s where s.epsilon.S is a single path representation.
Therefore, the expression transforming unit 224 transforms the expression according to the above described conversion rule, and obtains the state set string indicated by a single path representation. For example, when a computation tree logic expression AG (p.fwdarw.AFq) indicating the property to be verified through the input receipt unit 211 is input, the leading operator is the operator A indicating `universal`. Therefore, the negating unit 222 operates at an instruction from the operator determination unit 221, and first negates an input computation tree logic expression and then prepares it as shown in FIG. 1C, thereby obtaining a computation tree logic expression not including the operator A.
Furthermore, the initial state addition unit 223 adds the proposition logical expression pi corresponding to the initial state to the head of the computation tree logic expression to provide the obtained computation tree logic expression for use in the process to be performed by the expression transforming unit 224. In response to the input of the computation tree logic expression, the expression transforming unit 224 starts its operations to sequentially apply the above listed equations (8) and (9) to a partial expression indicated by each underline as shown in FIG. 1D. Thus, the single path representation shown in FIG. 1D can be obtained.
In the procedure string conversion unit 213, an expression transforming unit 226 converts a single path representation into the verification procedure string described below according to the conversion rule stored in a transform rule storage unit 227. A basic verification procedure string simply contains image computation. Equation (13) is represented from the following equation (11) using the propositions p and q, the operator Image indicating the image computation, and the operators gfp lfp indicating the largest floating point and the smallest floating point. EQU FindTrans(p)=Img(p) (11) EQU FindTrail(p,q)=1fp Z. [pImg(qZ)] (12) EQU FindLoop(p)=gfp Z. [pImg(Z)] (13)
The verification procedure FinfTrans(p) appearing in the above listed equation (11) is the very image computation. As shown in FIG. 1F, a reachable state set is returned in one state transition process from the state set represented by the proposition logic expression p. The verification procedure FindTrail(p,q) in the above listed equation (12) is a procedure of returning a state set (indicated by diagonal lines in FIG. 1G) reachable from the state set represented by the proposition logical expression p through a state set in which the proposition logical expression q exists as shown in FIG. 1G.
The verification procedure FindLoop(p) in the above listed equation (13) is a procedure of returning a union (indicated by diagonal lines in FIG. 1H) of a subset, which is contained in the state set represented by the proposition logical expression p as shown in FIG. 1H and forms a loop in which the proposition logical expression p exists, and a subset reachable from the loop. The transform rule storage unit 227 stores a conversion rule S represented by the following equations (14) through (18). EQU S(p)=p (14) EQU S(sp)=FindTrans(S(s))p (15) EQU S(sp*)=FindTrail(FindTrans(S(s),p)) (16) EQU S(sp.omega.)=FindLoop(FindTrail((S(s),p)p)) (17) EQU S({s.LAMBDA.p, sp*})=FindTrail(S(s),p) (18)
Therefore, the expression transforming unit 226 detects from the received single path representation a portion to which the conversion rules apply, and sequentially applies a corresponding conversion rule so that the single path representation can be converted into a verification procedure string. For example, in response to the single path representation shown in FIG. 1D, the expression transforming unit 226 sequentially applies the above listed equations (17) and (18) and prepares the equations to convert the representation into a procedure string as shown in FIG. 1E.
In response to the received procedure string, the set operation unit 214 performs an image computation and a floating point computation in the above listed equations 11 through 13, obtains a state set indicated by a single path representation, inputs it to the determining unit 215 to determine whether or not the state set is an empty set.
Since these procedure strings are executable using only image computation as described above, it can be verified whether or not a model of a logical device realizes the property which can be represented by a single path representation by performing a set operation process through the performance of a practical computer system even when the scale of a binary decision diagram is reduced by representing the state transition relation using a function.
Thus, relating to the property which can be represented by a single path representation, the memory requirements can be reduced and the process time can be shortened to solve the problems arising when a symbol model checking method is applied. As a result, the symbol model checking method can be applied to the property verification of a logical device having practical rules.
The above described conventional technologies have the following problems.
(1): In the symbol model checking method, the operation of a finite state machine is represented by a logical expression, and the verification procedure is realized in a logical function process. In this process, a binary decision diagram (BDD) is used as a representation format of a logical function. The number of states of the finite state machine used in the design verification may exceed 10.sup.20, and requires an implicit representation method using a logical function and an effective logical function process using the BDD.
However, when a process contains a number of states and a device processes complicated state transition, there arises the problem that the size of the BDD indicating the transition relation of a finite state machine and the size of the BDD generated during the logical function process are enlarged. The size of a BDD can be measured by the number of nodes of the BDD. In the worst case, a variable may increase like an index.
(2): The above described problem (1) can be attenuated by the property verification device (refer to Tokuganhei 8-220005). However, if the device is more complicated, the scale of the BDD may reach the limit. Relating to a part of the property, the scale of the BDD can be reduced by dividing the state set during the verification procedure (refer to reference documents 10 and 12). In this procedure, the state enumeration process (refer to reference document 5) is performed by repeating the image computation from the initial state within a limited storage capacity.
Since a common symbol model check is based on the inverse image computation (refer to reference document 5), this method is limited in application. On the other hand, since the above described property verification device (refer to Tokuganhei 8-220005) is based on the image computation, it is applicable in various fields. With the above described property verification device (refer to Tokuganhei 8-220005), the procedure of FindTrail() is based on the state enumeration, and can divide a state set for computation.
Furthermore, it is easy to divide a state set of FindTrans() for computation. However, FindLoop() refers to a procedure quite different from the state enumeration, and is not allowed to divide a state set for a process. Therefore, in most cases, the method of dividing a state set does not work for reduction of a storage capacity in the symbol model checking method.
.sctn.4: Reference documents.
(reference document 1): R. E. Bryant. Graph based algorithm for boolean function manipulation. IEEE Trans. Comput., C-35 (8): 677-691, 1986.
(reference document 2): E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Syst., 8 (2): 244-263, 1986.
(reference document 3): Fujita, Chen, and Yamazaki. Example of application to actual design of formal verification method. Information process, 35 (8): 719-725, 1994.
(reference document 4): Fujita and E. M. Clarke. Application of BDD to CAD. Information process, 34 (5): 609-616, 1993.
(reference document 5): Hiraishi and Hamaguchi. Formal verification method based on logical function process. Information process, 35 (8): 710-718, 1994.
(reference document 6): J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979.
(reference document 7): Minato. BDD process technology through computer. Information process, 34 (5): 593-599, 1993.
(reference document 8): Taniguchi and Kitamichi. Specification description, design, and verification through algebraic method. Information process. 35 (8): 742-750, 1994.
(reference document 9): Ishiura. What's BDD? Information process. 34 (5): 585-592, 1993.
(reference document 10): H. Iwashita, S. Kowatari, T. Nakata, and F. Hirose. Automatic test program generation for pipelined processors. In Proceedings of the International Conference on Computer-Aided Design, pp. 580-583, 1994.
(reference document 11): Kimura. Formal timing verification. Information process. 35 (8): 726-735, 1994.
(reference document 12): K. Ravi and R. Somenzi. High-density reachability analysis. In Proceedings of the International Conference on Computer-Aided Design, pp. 154-158, 1995.
(reference document 13): Takahara. Formal verification through process algebra. Information process. 35 (8): 736-741, 1994.
(reference document 14): Watanabe and Kukimoto. Application of BDD. Information process. 34 (5): 600-608, 1993.